\section{Konstrukcja sprawdzarki typów zależnych} \label{sec:kompilatory}
Rozdział opisuje różnicę między sprawdzeniem typów w kompilatorze języka prosto typowanego i zależnie typowanego. Przykładowe implementacje znajdują się w: \cite{lambdapi}, \cite{bauertutorial} oraz \cite{przemek} (implementacja powstała przy tworzeniu tej pracy).

\subsection{Wykonanie programu i generacja kodu wykonywalnego}
Programy odpowiadające twierdzeniom matematycznym (jak te przedstawione w tej pracy) zazwyczaj nie mają użytecznej interpretacji obliczeniowej, a jedynie mają dowieść poprawności twierdzenia. Dlatego sprawdzarka typów może nie generować kodu wynikowego (ani interpretować go), a tylko sprawdzać poprawność typów\footnote{Pod tym względem sprawdzarki znajdują się na przeciwnym końcu spektrum względem języków dynamicznie typowanych, które w ogóle nie sprawdzają typów w trakcie kompilacji, a ich użyteczność zależy tylko od generowanego kodu wynikowego lub interpretacji kodu.}.

\subsection{Normalizacja}
Normalizacja jest optymalizacją w kompilatorach języków prosto typowanych i koniecznością w kompilatorach języków zależnie typowanych. Dla przykładu rozpatruje się następujące definicje:
\begin{align*}
  C &: Bool \rightarrow \universe{0} \\
  C &\equiv \fnd{b : Bool}{if(\lambda b . \universe{0},\unittype,\nat,b)} \\
  f &: \unittype \rightarrow C(true) \\
  f &\equiv \lambda x . \ttt
\end{align*}
Nieznormalizowane AST dla deklaracji typu $f$ wygląda tak (używając stworzonego ad-hoc AST w postaci S-wyrażeń):
\begin{verbatim}
(Pi
  Unit-type
  (apply (val "C") (val "true")))
\end{verbatim}
a typ wywnioskowany z implementacji to $f$: \inlinecode{(Pi Unit-type Unit-type)}, czyli różny od zadeklarowanego. Ponadto sprawdzanie typu wyrażenia musi poprzedzać normalizację (podobnie jak dla kompilatorów języków prosto typowanych). Przykład: wyrażenie \(\left(f(false)\right)\) jest źle otypowane, lecz funkcja $f$ jest stała i całe wyrażenie mogłoby być przedwcześnie znormalizowane do $\ttt$.
